R-FeasibleWitness{i:l}
R-FeasibleWitness(R; sv; av; dis; cl; fr; sfr; rfr; afr; bfr)
== case R of 
== Rnone => Rnone() = Rnone()
== Rplus(left,right)=>rec1,rec2.rec1 & rec2
== Rinit(loc,T,x,v)=> cl(loc,<1, x>) = Rinit(loc;T;x;v) & sv(x) = <T, v> & dis(loc,x) = isl(v)
== Rframe(loc,T,x,L)=> cl(loc,<2, x>) = Rframe(loc;T;x;L) & ((sv(x)).1) = T & fr(loc,x) = L
== Rsframe(lnk,tag,L)=> cl(source(lnk),<3, lnk, tag>) = Rsframe(lnk;tag;L) & sfr(lnk,tag) = L
== Reffect(loc,ds,knd,T,x,f)=> cl(loc,<4, knd, x>) = Reffect(loc;ds;knd;T;x;f)
== & isl(f) = isl((sv(x)).2)
== & zdom(ds). A=ds(z)   ((sv(z)).1) = A & av(knd) = T
== & ((isrcv(knd))  (loc = destination(lnk(knd))))
== & (knd  fr(loc,x))
== & (zfpf-domain(ds). (knd  rfr(loc,z)))
== & dis(loc,x) = isl(f)
== & ((can-apply(afr(loc);knd))  (x  do-apply(afr(loc);knd)))
== Rsends(ds,knd,T,l,dt,g)=> cl(source(l),<5, knd, l>) = Rsends(ds;knd;T;l;dt;g)
== & ((isrcv(knd))
== & ( (((lnk(knd) = l)  (T = dt(tag(knd))?Void)) & destination(lnk(knd)) = source(l)))
== & zdom(ds). A=ds(z)   ((sv(z)).1) = A
== & av(knd) = T
== & kdom(lnk-decl(l;dt)). A=lnk-decl(l;dt)(k)   av(k) = A
== & Normal(dt)
== & (tgmap(p.p.1;g). (knd  sfr(l,tg)))
== & (zfpf-domain(ds). (knd  rfr(source(l),z)))
== & ((can-apply(bfr(source(l));knd))  (l  do-apply(bfr(source(l));knd)))
== Rpre(loc,ds,a,p,P)=> cl(loc,<6, a>) = Rpre(loc;ds;a;p;P)
== & zdom(ds). A=ds(z)   ((sv(z)).1) = A
== & av(locl(a)) = Outcome
== & (zfpf-domain(ds). (locl(a)  rfr(loc,z)))
== Rkframe(loc,k,L)=> cl(loc,<7, k>) = Raframe(loc;k;L) & afr(loc,k) = (inl L )
== Rksframe(loc,k,L)=> cl(loc,<8, k>) = Rbframe(loc;k;L) & bfr(loc,k) = (inl L )
== Rrframe(loc,x,L)=> cl(loc,<9, x>) = Rrframe(loc;x;L) & rfr(loc,x) = L 

latex

---

clarification:

R-FeasibleWitness{i:l}
R-FeasibleWitness(R; sv; av; dis; cl; fr; sfr; rfr; afr; bfr)
== case R of 
== Rnone => Rnone() = Rnone()  es_realizer{i:l}
== Rplus(left,right)=>rec1,rec2.rec1 & rec2
== Rinit(loc,T,x,v)=> cl(loc,<1, x>) = Rinit(loc;T;x;v)  es_realizer{i:l}
== & sv(x) = <T, v>  (A:Type{i}  (A + (A)))
== & dis(loc,x) = isl(v)  
== Rframe(loc,T,x,L)=> cl(loc,<2, x>) = Rframe(loc;T;x;L)  es_realizer{i:l}
== & ((sv(x)).1) = T  Type{i}
== & fr(loc,x) = L  (Knd List)
== Rsframe(lnk,tag,L)=> cl(source(lnk),<3, lnk, tag>) = Rsframe(lnk;tag;L)  es_realizer{i:l}
== & sfr(lnk,tag) = L  (Knd List)
== Reffect(loc,ds,knd,T,x,f)=> cl(loc,<4, knd, x>) = Reffect(loc;ds;knd;T;x;f)  es_realizer{i:l}
== & isl(f) = isl((sv(x)).2)  
== & IdIdDeqzdom(ds). A=ds(z)   ((sv(z)).1) = A  Type{i} & av(knd) = T  Type{i}
== & ((isrcv(knd))  (loc = destination(lnk(knd))  Id))
== & (knd  fr(loc,x)  Knd)
== & l_all(fpf-domain(ds);Id;z.(knd  rfr(loc,z)  Knd))
== & dis(loc,x) = isl(f)  
== & ((can-apply(afr(loc);knd))  (x  do-apply(afr(loc);knd)  Id))
== Rsends(ds,knd,T,l,dt,g)=> cl(source(l),<5, knd, l>) = Rsends(ds;knd;T;l;dt;g)  es_realizer{i:l}
== & ((isrcv(knd))
== & ( (((lnk(knd) = l)  (T = fpf-cap(dt;IdDeq;tag(knd);Void)  Type{i}))
== & ( & destination(lnk(knd)) = source(l)  Id))
== & IdIdDeqzdom(ds). A=ds(z)   ((sv(z)).1) = A  Type{i}
== & av(knd) = T  Type{i}
== & KndKindDeqkdom(lnk-decl(l;dt)). A=lnk-decl(l;dt)(k)   av(k) = A  Type{i}
== & normal-ds{i:l}
== & normal-ds(dt)
== & l_all(map(p.p.1;g);Id;tg.(knd  sfr(l,tg)  Knd))
== & l_all(fpf-domain(ds);Id;z.(knd  rfr(source(l),z)  Knd))
== & ((can-apply(bfr(source(l));knd))  (l  do-apply(bfr(source(l));knd)  IdLnk))
== Rpre(loc,ds,a,p,P)=> cl(loc,<6, a>) = Rpre(loc;ds;a;p;P)  es_realizer{i:l}
== & IdIdDeqzdom(ds). A=ds(z)   ((sv(z)).1) = A  Type{i}
== & av(locl(a)) = p-outcome(p)  Type{i}
== & l_all(fpf-domain(ds);Id;z.(locl(a)  rfr(loc,z)  Knd))
== Rkframe(loc,k,L)=> cl(loc,<7, k>) = Raframe(loc;k;L)  es_realizer{i:l}
== & afr(loc,k) = (inl L )  ((Id List) + Top)
== Rksframe(loc,k,L)=> cl(loc,<8, k>) = Rbframe(loc;k;L)  es_realizer{i:l}
== & bfr(loc,k) = (inl L )  ((IdLnk List) + Top)
== Rrframe(loc,x,L)=> cl(loc,<9, x>) = Rrframe(loc;x;L)  es_realizer{i:l}
== & rfr(loc,x) = L  (Knd List) 

latex

Definitions

es realizer ind, Rnone(), Rinit(loc;T;x;v), x:A  B(x), x:AB(x), , Rframe(loc;T;x;L), Rsframe(lnk;tag;L), Reffect(loc;ds;knd;T;x;f), t.2, , isl(x), Rsends(ds;knd;T;l;dt;g), isrcv(k), a = b, f(x)?z, tag(k), Void, destination(l), lnk(k), KindDeq, lnk-decl(l;dt), Normal(ds), map(f;as), x.A(x), P  Q, b, can-apply(f;x), do-apply(f;x), source(l), Rpre(loc;ds;a;p;P), xdom(f). v=f(x)   P(x;v), IdDeq, t.1, Type, Outcome, xL. P(x), fpf-domain(f), (x  l), locl(a), Raframe(loc;k;L), Id, Rbframe(loc;k;L), left + right, IdLnk, Top, inl x , P & Q, Realizer, <a, b>, #$n, Rrframe(loc;x;L), s = t, type List, Knd, f(a)